Left Termination proof of /tmp/tmplPVBWk/rev.pl

Left Termination of the query pattern
rev(g,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog

↳1 PrologToPrologProblemTransformerProof (⇒, 390 ms)

↳2 Prolog

↳3 PrologToPiTRSProof (⇒, 11 ms)

↳4 PiTRS

↳5 DependencyPairsProof (⇔, 0 ms)

↳6 PiDP

↳7 DependencyGraphProof (⇔, 0 ms)

↳8 PiDP

↳9 UsableRulesProof (⇔, 0 ms)

↳10 PiDP

↳11 PiDPToQDPProof (⇒, 5 ms)

↳12 QDP

↳13 QDPSizeChangeProof (⇔, 0 ms)

↳14 YES

(0) Obligation:

Clauses:

rev(L, R) :- rev(L, [], R).
rev([], Y, Z) :- ','(!, eq(Y, Z)).
rev(L, S, R) :- ','(head(L, X), ','(tail(L, T), rev(T, .(X, S), R))).
head([], X1).
head(.(X, X2), X).
tail([], []).
tail(.(X3, Xs), Xs).
eq(X, X).

Query: rev(g,a)

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph ICLP10.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: rev(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: rev(T1, T2), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: rev(T5, [], T7)\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: rev(T5, [], T7), SCOPE: 2, CLAUSE: 1 | rev(T5, [], T7), SCOPE: 2, CLAUSE: 2\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: ','(!_2, eq([], T11)) | rev([], [], T7), SCOPE: 2, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: rev(T5, [], T7), SCOPE: 2, CLAUSE: 2\n\nT5 is ground\nX12 is free\nX13 is free\nrev(T5, [], T7) !=? rev([], X12, X13)", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: eq([], T11)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: eq([], T11), SCOPE: 3, CLAUSE: 7\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(head(T18, X31), ','(tail(T18, X32), rev(X32, .(X31, []), T20)))\n\nT18 is ground\nX12 is free\nX13 is free\nX31 is free\nX32 is free\nrev(T18, [], T7) !=? rev([], X12, X13)", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(head(T18, X31), ','(tail(T18, X32), rev(X32, .(X31, []), T20))), SCOPE: 4, CLAUSE: 3 | ','(head(T18, X31), ','(tail(T18, X32), rev(X32, .(X31, []), T20))), SCOPE: 4, CLAUSE: 4\n\nT18 is ground\nX12 is free\nX13 is free\nX31 is free\nX32 is free\nrev(T18, [], T7) !=? rev([], X12, X13)", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(head(T18, X31), ','(tail(T18, X32), rev(X32, .(X31, []), T20))), SCOPE: 4, CLAUSE: 4\n\nT18 is ground\nX12 is free\nX13 is free\nX31 is free\nX32 is free\nrev(T18, [], T7) !=? rev([], X12, X13)", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(tail(.(T26, T27), X32), rev(X32, .(T26, []), T20))\n\nT26 is ground\nT27 is ground\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(tail(.(T26, T27), X32), rev(X32, .(T26, []), T20)), SCOPE: 5, CLAUSE: 5 | ','(tail(.(T26, T27), X32), rev(X32, .(T26, []), T20)), SCOPE: 5, CLAUSE: 6\n\nT26 is ground\nT27 is ground\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(tail(.(T26, T27), X32), rev(X32, .(T26, []), T20)), SCOPE: 5, CLAUSE: 6\n\nT26 is ground\nT27 is ground\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: rev(T37, .(T36, []), T20)\n\nT36 is ground\nT37 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: rev(T37, .(T36, []), T20), SCOPE: 6, CLAUSE: 1 | rev(T37, .(T36, []), T20), SCOPE: 6, CLAUSE: 2\n\nT36 is ground\nT37 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: ','(!_6, eq(.(T44, []), T46)) | rev([], .(T44, []), T20), SCOPE: 6, CLAUSE: 2\n\nT44 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: rev(T37, .(T36, []), T20), SCOPE: 6, CLAUSE: 2\n\nT36 is ground\nT37 is ground\nX60 is free\nX61 is free\nrev(T37, .(T36, []), T20) !=? rev([], X60, X61)", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: eq(.(T44, []), T46)\n\nT44 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: eq(.(T44, []), T46), SCOPE: 7, CLAUSE: 7\n\nT44 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(head(T59, X79), ','(tail(T59, X80), rev(X80, .(X79, .(T60, [])), T62)))\n\nT59 is ground\nT60 is ground\nX60 is free\nX61 is free\nX79 is free\nX80 is free\nrev(T59, .(T60, []), T20) !=? rev([], X60, X61)", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(head(T59, X79), ','(tail(T59, X80), rev(X80, .(X79, .(T60, [])), T62))), SCOPE: 8, CLAUSE: 3 | ','(head(T59, X79), ','(tail(T59, X80), rev(X80, .(X79, .(T60, [])), T62))), SCOPE: 8, CLAUSE: 4\n\nT59 is ground\nT60 is ground\nX60 is free\nX61 is free\nX79 is free\nX80 is free\nrev(T59, .(T60, []), T20) !=? rev([], X60, X61)", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(head(T59, X79), ','(tail(T59, X80), rev(X80, .(X79, .(T60, [])), T62))), SCOPE: 8, CLAUSE: 4\n\nT59 is ground\nT60 is ground\nX60 is free\nX61 is free\nX79 is free\nX80 is free\nrev(T59, .(T60, []), T20) !=? rev([], X60, X61)", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(tail(.(T69, T70), X80), rev(X80, .(T69, .(T60, [])), T62))\n\nT60 is ground\nT69 is ground\nT70 is ground\nX80 is free", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ','(tail(.(T69, T70), X80), rev(X80, .(T69, .(T60, [])), T62)), SCOPE: 9, CLAUSE: 5 | ','(tail(.(T69, T70), X80), rev(X80, .(T69, .(T60, [])), T62)), SCOPE: 9, CLAUSE: 6\n\nT60 is ground\nT69 is ground\nT70 is ground\nX80 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ','(tail(.(T69, T70), X80), rev(X80, .(T69, .(T60, [])), T62)), SCOPE: 9, CLAUSE: 6\n\nT60 is ground\nT69 is ground\nT70 is ground\nX80 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: rev(T82, .(T81, .(T60, [])), T62)\n\nT60 is ground\nT81 is ground\nT82 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: rev(T82, .(T81, .(T60, [])), T62), SCOPE: 10, CLAUSE: 1 | rev(T82, .(T81, .(T60, [])), T62), SCOPE: 10, CLAUSE: 2\n\nT60 is ground\nT81 is ground\nT82 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(!_10, eq(.(T92, .(T93, [])), T95)) | rev([], .(T92, .(T93, [])), T62), SCOPE: 10, CLAUSE: 2\n\nT92 is ground\nT93 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: rev(T82, .(T81, .(T60, [])), T62), SCOPE: 10, CLAUSE: 2\n\nT60 is ground\nT81 is ground\nT82 is ground\nX108 is free\nX109 is free\nrev(T82, .(T81, .(T60, [])), T62) !=? rev([], X108, X109)", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: eq(.(T92, .(T93, [])), T95)\n\nT92 is ground\nT93 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: eq(.(T92, .(T93, [])), T95), SCOPE: 11, CLAUSE: 7\n\nT92 is ground\nT93 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ','(head(T114, X127), ','(tail(T114, X128), rev(X128, .(X127, .(T115, .(T116, []))), T118)))\n\nT114 is ground\nT115 is ground\nT116 is ground\nX108 is free\nX109 is free\nX127 is free\nX128 is free\nrev(T114, .(T115, .(T116, [])), T62) !=? rev([], X108, X109)", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: ','(head(T114, X127), ','(tail(T114, X128), rev(X128, .(X127, .(T115, .(T116, []))), T118))), SCOPE: 12, CLAUSE: 3 | ','(head(T114, X127), ','(tail(T114, X128), rev(X128, .(X127, .(T115, .(T116, []))), T118))), SCOPE: 12, CLAUSE: 4\n\nT114 is ground\nT115 is ground\nT116 is ground\nX108 is free\nX109 is free\nX127 is free\nX128 is free\nrev(T114, .(T115, .(T116, [])), T62) !=? rev([], X108, X109)", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: ','(head(T114, X127), ','(tail(T114, X128), rev(X128, .(X127, .(T115, .(T116, []))), T118))), SCOPE: 12, CLAUSE: 4\n\nT114 is ground\nT115 is ground\nT116 is ground\nX108 is free\nX109 is free\nX127 is free\nX128 is free\nrev(T114, .(T115, .(T116, [])), T62) !=? rev([], X108, X109)", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: ','(tail(.(T126, T127), X128), rev(X128, .(T126, .(T115, .(T116, []))), T118))\n\nT115 is ground\nT116 is ground\nT126 is ground\nT127 is ground\nX128 is free", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(tail(.(T126, T127), X128), rev(X128, .(T126, .(T115, .(T116, []))), T118)), SCOPE: 13, CLAUSE: 5 | ','(tail(.(T126, T127), X128), rev(X128, .(T126, .(T115, .(T116, []))), T118)), SCOPE: 13, CLAUSE: 6\n\nT115 is ground\nT116 is ground\nT126 is ground\nT127 is ground\nX128 is free", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(tail(.(T126, T127), X128), rev(X128, .(T126, .(T115, .(T116, []))), T118)), SCOPE: 13, CLAUSE: 6\n\nT115 is ground\nT116 is ground\nT126 is ground\nT127 is ground\nX128 is free", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: rev(T141, .(T140, .(T115, .(T116, []))), T118)\n\nT115 is ground\nT116 is ground\nT140 is ground\nT141 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: rev(T141, .(T140, .(T115, .(T116, []))), T118), SCOPE: 14, CLAUSE: 1 | rev(T141, .(T140, .(T115, .(T116, []))), T118), SCOPE: 14, CLAUSE: 2\n\nT115 is ground\nT116 is ground\nT140 is ground\nT141 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: ','(!_14, eq(.(T154, .(T155, .(T156, []))), T158)) | rev([], .(T154, .(T155, .(T156, []))), T118), SCOPE: 14, CLAUSE: 2\n\nT154 is ground\nT155 is ground\nT156 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: rev(T141, .(T140, .(T115, .(T116, []))), T118), SCOPE: 14, CLAUSE: 2\n\nT115 is ground\nT116 is ground\nT140 is ground\nT141 is ground\nX156 is free\nX157 is free\nrev(T141, .(T140, .(T115, .(T116, []))), T118) !=? rev([], X156, X157)", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: eq(.(T154, .(T155, .(T156, []))), T158)\n\nT154 is ground\nT155 is ground\nT156 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: eq(.(T154, .(T155, .(T156, []))), T158), SCOPE: 15, CLAUSE: 7\n\nT154 is ground\nT155 is ground\nT156 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(head(T183, X175), ','(tail(T183, X176), rev(X176, .(X175, .(T184, .(T185, .(T186, [])))), T188)))\n\nT183 is ground\nT184 is ground\nT185 is ground\nT186 is ground\nX156 is free\nX157 is free\nX175 is free\nX176 is free\nrev(T183, .(T184, .(T185, .(T186, []))), T118) !=? rev([], X156, X157)", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: ','(head(T183, X175), ','(tail(T183, X176), rev(X176, .(X175, .(T184, .(T185, .(T186, [])))), T188))), SCOPE: 16, CLAUSE: 3 | ','(head(T183, X175), ','(tail(T183, X176), rev(X176, .(X175, .(T184, .(T185, .(T186, [])))), T188))), SCOPE: 16, CLAUSE: 4\n\nT183 is ground\nT184 is ground\nT185 is ground\nT186 is ground\nX156 is free\nX157 is free\nX175 is free\nX176 is free\nrev(T183, .(T184, .(T185, .(T186, []))), T118) !=? rev([], X156, X157)", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ','(head(T183, X175), ','(tail(T183, X176), rev(X176, .(X175, .(T184, .(T185, .(T186, [])))), T188))), SCOPE: 16, CLAUSE: 4\n\nT183 is ground\nT184 is ground\nT185 is ground\nT186 is ground\nX156 is free\nX157 is free\nX175 is free\nX176 is free\nrev(T183, .(T184, .(T185, .(T186, []))), T118) !=? rev([], X156, X157)", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: ','(tail(.(T197, T198), X176), rev(X176, .(T197, .(T184, .(T185, .(T186, [])))), T188))\n\nT184 is ground\nT185 is ground\nT186 is ground\nT197 is ground\nT198 is ground\nX176 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: ','(tail(.(T197, T198), X176), rev(X176, .(T197, .(T184, .(T185, .(T186, [])))), T188)), SCOPE: 17, CLAUSE: 5 | ','(tail(.(T197, T198), X176), rev(X176, .(T197, .(T184, .(T185, .(T186, [])))), T188)), SCOPE: 17, CLAUSE: 6\n\nT184 is ground\nT185 is ground\nT186 is ground\nT197 is ground\nT198 is ground\nX176 is free", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: ','(tail(.(T197, T198), X176), rev(X176, .(T197, .(T184, .(T185, .(T186, [])))), T188)), SCOPE: 17, CLAUSE: 6\n\nT184 is ground\nT185 is ground\nT186 is ground\nT197 is ground\nT198 is ground\nX176 is free", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: rev(T214, .(T213, .(T184, .(T185, .(T186, [])))), T188)\n\nT184 is ground\nT185 is ground\nT186 is ground\nT213 is ground\nT214 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: rev(T214, .(T213, .(T184, .(T185, .(T186, [])))), T188), SCOPE: 18, CLAUSE: 1 | rev(T214, .(T213, .(T184, .(T185, .(T186, [])))), T188), SCOPE: 18, CLAUSE: 2\n\nT184 is ground\nT185 is ground\nT186 is ground\nT213 is ground\nT214 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: ','(!_18, eq(.(T230, .(T231, .(T232, .(T233, [])))), T235)) | rev([], .(T230, .(T231, .(T232, .(T233, [])))), T188), SCOPE: 18, CLAUSE: 2\n\nT230 is ground\nT231 is ground\nT232 is ground\nT233 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: rev(T214, .(T213, .(T184, .(T185, .(T186, [])))), T188), SCOPE: 18, CLAUSE: 2\n\nT184 is ground\nT185 is ground\nT186 is ground\nT213 is ground\nT214 is ground\nX204 is free\nX205 is free\nrev(T214, .(T213, .(T184, .(T185, .(T186, [])))), T188) !=? rev([], X204, X205)", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: eq(.(T230, .(T231, .(T232, .(T233, [])))), T235)\n\nT230 is ground\nT231 is ground\nT232 is ground\nT233 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: eq(.(T230, .(T231, .(T232, .(T233, [])))), T235), SCOPE: 19, CLAUSE: 7\n\nT230 is ground\nT231 is ground\nT232 is ground\nT233 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ','(head(T266, X223), ','(tail(T266, X224), rev(X224, .(X223, .(T267, .(T268, .(T269, .(T270, []))))), T272)))\n\nT266 is ground\nT267 is ground\nT268 is ground\nT269 is ground\nT270 is ground\nX204 is free\nX205 is free\nX223 is free\nX224 is free\nrev(T266, .(T267, .(T268, .(T269, .(T270, [])))), T188) !=? rev([], X204, X205)", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: ','(head(T266, X223), ','(tail(T266, X224), rev(X224, .(X223, .(T267, .(T268, .(T269, .(T270, []))))), T272))), SCOPE: 20, CLAUSE: 3 | ','(head(T266, X223), ','(tail(T266, X224), rev(X224, .(X223, .(T267, .(T268, .(T269, .(T270, []))))), T272))), SCOPE: 20, CLAUSE: 4\n\nT266 is ground\nT267 is ground\nT268 is ground\nT269 is ground\nT270 is ground\nX204 is free\nX205 is free\nX223 is free\nX224 is free\nrev(T266, .(T267, .(T268, .(T269, .(T270, [])))), T188) !=? rev([], X204, X205)", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: ','(head(T266, X223), ','(tail(T266, X224), rev(X224, .(X223, .(T267, .(T268, .(T269, .(T270, []))))), T272))), SCOPE: 20, CLAUSE: 4\n\nT266 is ground\nT267 is ground\nT268 is ground\nT269 is ground\nT270 is ground\nX204 is free\nX205 is free\nX223 is free\nX224 is free\nrev(T266, .(T267, .(T268, .(T269, .(T270, [])))), T188) !=? rev([], X204, X205)", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(tail(.(T282, T283), X224), rev(X224, .(T282, .(T267, .(T268, .(T269, .(T270, []))))), T272))\n\nT267 is ground\nT268 is ground\nT269 is ground\nT270 is ground\nT282 is ground\nT283 is ground\nX224 is free", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: ','(tail(.(T282, T283), X224), rev(X224, .(T282, .(T267, .(T268, .(T269, .(T270, []))))), T272)), SCOPE: 21, CLAUSE: 5 | ','(tail(.(T282, T283), X224), rev(X224, .(T282, .(T267, .(T268, .(T269, .(T270, []))))), T272)), SCOPE: 21, CLAUSE: 6\n\nT267 is ground\nT268 is ground\nT269 is ground\nT270 is ground\nT282 is ground\nT283 is ground\nX224 is free", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: ','(tail(.(T282, T283), X224), rev(X224, .(T282, .(T267, .(T268, .(T269, .(T270, []))))), T272)), SCOPE: 21, CLAUSE: 6\n\nT267 is ground\nT268 is ground\nT269 is ground\nT270 is ground\nT282 is ground\nT283 is ground\nX224 is free", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: rev(T301, .(T300, .(T267, .(T268, .(T269, .(T270, []))))), T272)\n\nT267 is ground\nT268 is ground\nT269 is ground\nT270 is ground\nT300 is ground\nT301 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: rev(T301, .(T300, .(T267, .(T268, .(T269, .(T270, []))))), T272), SCOPE: 22, CLAUSE: 1 | rev(T301, .(T300, .(T267, .(T268, .(T269, .(T270, []))))), T272), SCOPE: 22, CLAUSE: 2\n\nT267 is ground\nT268 is ground\nT269 is ground\nT270 is ground\nT300 is ground\nT301 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ','(!_22, eq(.(T320, .(T321, .(T322, .(T323, .(T324, []))))), T326)) | rev([], .(T320, .(T321, .(T322, .(T323, .(T324, []))))), T272), SCOPE: 22, CLAUSE: 2\n\nT320 is ground\nT321 is ground\nT322 is ground\nT323 is ground\nT324 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: rev(T301, .(T300, .(T267, .(T268, .(T269, .(T270, []))))), T272), SCOPE: 22, CLAUSE: 2\n\nT267 is ground\nT268 is ground\nT269 is ground\nT270 is ground\nT300 is ground\nT301 is ground\nX252 is free\nX253 is free\nrev(T301, .(T300, .(T267, .(T268, .(T269, .(T270, []))))), T272) !=? rev([], X252, X253)", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: eq(.(T320, .(T321, .(T322, .(T323, .(T324, []))))), T326)\n\nT320 is ground\nT321 is ground\nT322 is ground\nT323 is ground\nT324 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: eq(.(T320, .(T321, .(T322, .(T323, .(T324, []))))), T326), SCOPE: 23, CLAUSE: 7\n\nT320 is ground\nT321 is ground\nT322 is ground\nT323 is ground\nT324 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ','(head(T363, X271), ','(tail(T363, X272), rev(X272, .(X271, .(T364, .(T365, .(T366, .(T367, .(T368, [])))))), T370)))\n\nT363 is ground\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT368 is ground\nX252 is free\nX253 is free\nX271 is free\nX272 is free\nrev(T363, .(T364, .(T365, .(T366, .(T367, .(T368, []))))), T272) !=? rev([], X252, X253)", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: ','(head(T363, X271), ','(tail(T363, X272), rev(X272, .(X271, .(T364, .(T365, .(T366, .(T367, .(T368, [])))))), T370))), SCOPE: 24, CLAUSE: 3 | ','(head(T363, X271), ','(tail(T363, X272), rev(X272, .(X271, .(T364, .(T365, .(T366, .(T367, .(T368, [])))))), T370))), SCOPE: 24, CLAUSE: 4\n\nT363 is ground\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT368 is ground\nX252 is free\nX253 is free\nX271 is free\nX272 is free\nrev(T363, .(T364, .(T365, .(T366, .(T367, .(T368, []))))), T272) !=? rev([], X252, X253)", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: ','(head(T363, X271), ','(tail(T363, X272), rev(X272, .(X271, .(T364, .(T365, .(T366, .(T367, .(T368, [])))))), T370))), SCOPE: 24, CLAUSE: 4\n\nT363 is ground\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT368 is ground\nX252 is free\nX253 is free\nX271 is free\nX272 is free\nrev(T363, .(T364, .(T365, .(T366, .(T367, .(T368, []))))), T272) !=? rev([], X252, X253)", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: ','(tail(.(T381, T382), X272), rev(X272, .(T381, .(T364, .(T365, .(T366, .(T367, .(T368, [])))))), T370))\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT368 is ground\nT381 is ground\nT382 is ground\nX272 is free", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(tail(.(T381, T382), X272), rev(X272, .(T381, .(T364, .(T365, .(T366, .(T367, .(T368, [])))))), T370)), SCOPE: 25, CLAUSE: 5 | ','(tail(.(T381, T382), X272), rev(X272, .(T381, .(T364, .(T365, .(T366, .(T367, .(T368, [])))))), T370)), SCOPE: 25, CLAUSE: 6\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT368 is ground\nT381 is ground\nT382 is ground\nX272 is free", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: ','(tail(.(T381, T382), X272), rev(X272, .(T381, .(T364, .(T365, .(T366, .(T367, .(T368, [])))))), T370)), SCOPE: 25, CLAUSE: 6\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT368 is ground\nT381 is ground\nT382 is ground\nX272 is free", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: rev(T402, .(T401, .(T364, .(T365, .(T366, .(T367, .(T368, [])))))), T370)\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT368 is ground\nT401 is ground\nT402 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: rev(T402, .(T401, .(T364, .(T365, .(T366, .(T367, .(T368, [])))))), T370), SCOPE: 26, CLAUSE: 1 | rev(T402, .(T401, .(T364, .(T365, .(T366, .(T367, .(T368, [])))))), T370), SCOPE: 26, CLAUSE: 2\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT368 is ground\nT401 is ground\nT402 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: ','(!_26, eq(.(T424, .(T425, .(T426, .(T427, .(T428, .(T429, [])))))), T431)) | rev([], .(T424, .(T425, .(T426, .(T427, .(T428, .(T429, [])))))), T370), SCOPE: 26, CLAUSE: 2\n\nT424 is ground\nT425 is ground\nT426 is ground\nT427 is ground\nT428 is ground\nT429 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: rev(T402, .(T401, .(T364, .(T365, .(T366, .(T367, .(T368, [])))))), T370), SCOPE: 26, CLAUSE: 2\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT368 is ground\nT401 is ground\nT402 is ground\nX300 is free\nX301 is free\nrev(T402, .(T401, .(T364, .(T365, .(T366, .(T367, .(T368, [])))))), T370) !=? rev([], X300, X301)", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: eq(.(T424, .(T425, .(T426, .(T427, .(T428, .(T429, [])))))), T431)\n\nT424 is ground\nT425 is ground\nT426 is ground\nT427 is ground\nT428 is ground\nT429 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: eq(.(T424, .(T425, .(T426, .(T427, .(T428, .(T429, [])))))), T431), SCOPE: 27, CLAUSE: 7\n\nT424 is ground\nT425 is ground\nT426 is ground\nT427 is ground\nT428 is ground\nT429 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: ','(head(T474, X319), ','(tail(T474, X320), rev(X320, .(X319, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, []))))))), T482)))\n\nT474 is ground\nT475 is ground\nT476 is ground\nT477 is ground\nT478 is ground\nT479 is ground\nT480 is ground\nX300 is free\nX301 is free\nX319 is free\nX320 is free\nrev(T474, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, [])))))), T370) !=? rev([], X300, X301)", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: ','(head(T474, X319), ','(tail(T474, X320), rev(X320, .(X319, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, []))))))), T482))), SCOPE: 28, CLAUSE: 3 | ','(head(T474, X319), ','(tail(T474, X320), rev(X320, .(X319, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, []))))))), T482))), SCOPE: 28, CLAUSE: 4\n\nT474 is ground\nT475 is ground\nT476 is ground\nT477 is ground\nT478 is ground\nT479 is ground\nT480 is ground\nX300 is free\nX301 is free\nX319 is free\nX320 is free\nrev(T474, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, [])))))), T370) !=? rev([], X300, X301)", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: ','(head(T474, X319), ','(tail(T474, X320), rev(X320, .(X319, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, []))))))), T482))), SCOPE: 28, CLAUSE: 4\n\nT474 is ground\nT475 is ground\nT476 is ground\nT477 is ground\nT478 is ground\nT479 is ground\nT480 is ground\nX300 is free\nX301 is free\nX319 is free\nX320 is free\nrev(T474, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, [])))))), T370) !=? rev([], X300, X301)", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: ','(tail(.(T494, T495), X320), rev(X320, .(T494, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, []))))))), T482))\n\nT475 is ground\nT476 is ground\nT477 is ground\nT478 is ground\nT479 is ground\nT480 is ground\nT494 is ground\nT495 is ground\nX320 is free", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: ','(tail(.(T494, T495), X320), rev(X320, .(T494, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, []))))))), T482)), SCOPE: 29, CLAUSE: 5 | ','(tail(.(T494, T495), X320), rev(X320, .(T494, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, []))))))), T482)), SCOPE: 29, CLAUSE: 6\n\nT475 is ground\nT476 is ground\nT477 is ground\nT478 is ground\nT479 is ground\nT480 is ground\nT494 is ground\nT495 is ground\nX320 is free", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: ','(tail(.(T494, T495), X320), rev(X320, .(T494, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, []))))))), T482)), SCOPE: 29, CLAUSE: 6\n\nT475 is ground\nT476 is ground\nT477 is ground\nT478 is ground\nT479 is ground\nT480 is ground\nT494 is ground\nT495 is ground\nX320 is free", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: rev(T517, .(T516, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, []))))))), T482)\n\nT475 is ground\nT476 is ground\nT477 is ground\nT478 is ground\nT479 is ground\nT480 is ground\nT516 is ground\nT517 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: rev(T517, .(T516, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, []))))))), T482), SCOPE: 30, CLAUSE: 1 | rev(T517, .(T516, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, []))))))), T482), SCOPE: 30, CLAUSE: 2\n\nT475 is ground\nT476 is ground\nT477 is ground\nT478 is ground\nT479 is ground\nT480 is ground\nT516 is ground\nT517 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: ','(!_30, eq(.(T542, .(T543, .(T544, .(T545, .(T546, .(T547, .(T548, []))))))), T550)) | rev([], .(T542, .(T543, .(T544, .(T545, .(T546, .(T547, .(T548, []))))))), T482), SCOPE: 30, CLAUSE: 2\n\nT542 is ground\nT543 is ground\nT544 is ground\nT545 is ground\nT546 is ground\nT547 is ground\nT548 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: rev(T517, .(T516, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, []))))))), T482), SCOPE: 30, CLAUSE: 2\n\nT475 is ground\nT476 is ground\nT477 is ground\nT478 is ground\nT479 is ground\nT480 is ground\nT516 is ground\nT517 is ground\nX348 is free\nX349 is free\nrev(T517, .(T516, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, []))))))), T482) !=? rev([], X348, X349)", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: eq(.(T542, .(T543, .(T544, .(T545, .(T546, .(T547, .(T548, []))))))), T550)\n\nT542 is ground\nT543 is ground\nT544 is ground\nT545 is ground\nT546 is ground\nT547 is ground\nT548 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: eq(.(T542, .(T543, .(T544, .(T545, .(T546, .(T547, .(T548, []))))))), T550), SCOPE: 31, CLAUSE: 7\n\nT542 is ground\nT543 is ground\nT544 is ground\nT545 is ground\nT546 is ground\nT547 is ground\nT548 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: ','(head(T599, X367), ','(tail(T599, X368), rev(X368, .(X367, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, [])))))))), T608)))\n\nT599 is ground\nT600 is ground\nT601 is ground\nT602 is ground\nT603 is ground\nT604 is ground\nT605 is ground\nT606 is ground\nX348 is free\nX349 is free\nX367 is free\nX368 is free\nrev(T599, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, []))))))), T482) !=? rev([], X348, X349)", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: ','(head(T599, X367), ','(tail(T599, X368), rev(X368, .(X367, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, [])))))))), T608))), SCOPE: 32, CLAUSE: 3 | ','(head(T599, X367), ','(tail(T599, X368), rev(X368, .(X367, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, [])))))))), T608))), SCOPE: 32, CLAUSE: 4\n\nT599 is ground\nT600 is ground\nT601 is ground\nT602 is ground\nT603 is ground\nT604 is ground\nT605 is ground\nT606 is ground\nX348 is free\nX349 is free\nX367 is free\nX368 is free\nrev(T599, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, []))))))), T482) !=? rev([], X348, X349)", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: ','(head(T599, X367), ','(tail(T599, X368), rev(X368, .(X367, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, [])))))))), T608))), SCOPE: 32, CLAUSE: 4\n\nT599 is ground\nT600 is ground\nT601 is ground\nT602 is ground\nT603 is ground\nT604 is ground\nT605 is ground\nT606 is ground\nX348 is free\nX349 is free\nX367 is free\nX368 is free\nrev(T599, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, []))))))), T482) !=? rev([], X348, X349)", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: ','(tail(.(T621, T622), X368), rev(X368, .(T621, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, [])))))))), T608))\n\nT600 is ground\nT601 is ground\nT602 is ground\nT603 is ground\nT604 is ground\nT605 is ground\nT606 is ground\nT621 is ground\nT622 is ground\nX368 is free", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: ','(tail(.(T621, T622), X368), rev(X368, .(T621, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, [])))))))), T608)), SCOPE: 33, CLAUSE: 5 | ','(tail(.(T621, T622), X368), rev(X368, .(T621, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, [])))))))), T608)), SCOPE: 33, CLAUSE: 6\n\nT600 is ground\nT601 is ground\nT602 is ground\nT603 is ground\nT604 is ground\nT605 is ground\nT606 is ground\nT621 is ground\nT622 is ground\nX368 is free", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: ','(tail(.(T621, T622), X368), rev(X368, .(T621, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, [])))))))), T608)), SCOPE: 33, CLAUSE: 6\n\nT600 is ground\nT601 is ground\nT602 is ground\nT603 is ground\nT604 is ground\nT605 is ground\nT606 is ground\nT621 is ground\nT622 is ground\nX368 is free", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: rev(T646, .(T645, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, [])))))))), T608)\n\nT600 is ground\nT601 is ground\nT602 is ground\nT603 is ground\nT604 is ground\nT605 is ground\nT606 is ground\nT645 is ground\nT646 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: rev(T646, .(T645, T656), T608)\n\nT645 is ground\nT646 is ground\nT656 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: rev(T646, .(T645, T656), T608), SCOPE: 34, CLAUSE: 1 | rev(T646, .(T645, T656), T608), SCOPE: 34, CLAUSE: 2\n\nT645 is ground\nT646 is ground\nT656 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: ','(!_34, eq(.(T666, T667), T669)) | rev([], .(T666, T667), T608), SCOPE: 34, CLAUSE: 2\n\nT666 is ground\nT667 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: rev(T646, .(T645, T656), T608), SCOPE: 34, CLAUSE: 2\n\nT645 is ground\nT646 is ground\nT656 is ground\nX398 is free\nX399 is free\nrev(T646, .(T645, T656), T608) !=? rev([], X398, X399)", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: eq(.(T666, T667), T669)\n\nT666 is ground\nT667 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: eq(.(T666, T667), T669), SCOPE: 35, CLAUSE: 7\n\nT666 is ground\nT667 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: ','(head(T688, X417), ','(tail(T688, X418), rev(X418, .(X417, .(T689, T690)), T692)))\n\nT688 is ground\nT689 is ground\nT690 is ground\nX398 is free\nX399 is free\nX417 is free\nX418 is free\nrev(T688, .(T689, T690), T608) !=? rev([], X398, X399)", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: ','(head(T688, X417), ','(tail(T688, X418), rev(X418, .(X417, .(T689, T690)), T692))), SCOPE: 36, CLAUSE: 3 | ','(head(T688, X417), ','(tail(T688, X418), rev(X418, .(X417, .(T689, T690)), T692))), SCOPE: 36, CLAUSE: 4\n\nT688 is ground\nT689 is ground\nT690 is ground\nX398 is free\nX399 is free\nX417 is free\nX418 is free\nrev(T688, .(T689, T690), T608) !=? rev([], X398, X399)", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: ','(head(T688, X417), ','(tail(T688, X418), rev(X418, .(X417, .(T689, T690)), T692))), SCOPE: 36, CLAUSE: 4\n\nT688 is ground\nT689 is ground\nT690 is ground\nX398 is free\nX399 is free\nX417 is free\nX418 is free\nrev(T688, .(T689, T690), T608) !=? rev([], X398, X399)", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: ','(tail(.(T700, T701), X418), rev(X418, .(T700, .(T689, T690)), T692))\n\nT689 is ground\nT690 is ground\nT700 is ground\nT701 is ground\nX418 is free", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: ','(tail(.(T700, T701), X418), rev(X418, .(T700, .(T689, T690)), T692)), SCOPE: 37, CLAUSE: 5 | ','(tail(.(T700, T701), X418), rev(X418, .(T700, .(T689, T690)), T692)), SCOPE: 37, CLAUSE: 6\n\nT689 is ground\nT690 is ground\nT700 is ground\nT701 is ground\nX418 is free", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: ','(tail(.(T700, T701), X418), rev(X418, .(T700, .(T689, T690)), T692)), SCOPE: 37, CLAUSE: 6\n\nT689 is ground\nT690 is ground\nT700 is ground\nT701 is ground\nX418 is free", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: rev(T715, .(T714, .(T689, T690)), T692)\n\nT689 is ground\nT690 is ground\nT714 is ground\nT715 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 149 [arrowhead = none ];
149 -> 2;

150 [label="ONLY EVAL with clause\nrev(X6, X7) :- rev(X6, [], X7).\nand substitutionT1 -> T5,\nX6 -> T5,\nT2 -> T7,\nX7 -> T7,\nT6 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 150 [arrowhead = none ];
150 -> 3;

151 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 151 [arrowhead = none ];
151 -> 4;

152 [label="EVAL with clause\nrev([], X12, X13) :- ','(!_2, eq(X12, X13)).\nand substitutionT5 -> [],\nX12 -> [],\nT7 -> T11,\nX13 -> T11,\nT10 -> T11", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 152 [arrowhead = none ];
152 -> 5;

153 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
4 -> 153 [arrowhead = none ];
153 -> 6;

154 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
5 -> 154 [arrowhead = none ];
154 -> 7;

155 [label="ONLY EVAL with clause\nrev(X28, X29, X30) :- ','(head(X28, X31), ','(tail(X28, X32), rev(X32, .(X31, X29), X30))).\nand substitutionT5 -> T18,\nX28 -> T18,\nX29 -> [],\nT7 -> T20,\nX30 -> T20,\nT19 -> T20", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 155 [arrowhead = none ];
155 -> 12;

156 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
7 -> 156 [arrowhead = none ];
156 -> 8;

157 [label="EVAL with clause\neq(X16, X16).\nand substitutionX16 -> [],\nT11 -> []", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 157 [arrowhead = none ];
157 -> 9;

158 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
8 -> 158 [arrowhead = none ];
158 -> 10;

159 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
9 -> 159 [arrowhead = none ];
159 -> 11;

160 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
12 -> 160 [arrowhead = none ];
160 -> 13;

161 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (rev(T18, [], T7), rev([], X12, X13))", fontsize=14, style = filled, fillcolor = lightgreen];
13 -> 161 [arrowhead = none ];
161 -> 14;

162 [label="EVAL with clause\nhead(.(X42, X43), X42).\nand substitutionX42 -> T26,\nX43 -> T27,\nT18 -> .(T26, T27),\nX31 -> T26", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 162 [arrowhead = none ];
162 -> 15;

163 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
14 -> 163 [arrowhead = none ];
163 -> 16;

164 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
15 -> 164 [arrowhead = none ];
164 -> 17;

165 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 165 [arrowhead = none ];
165 -> 18;

166 [label="ONLY EVAL with clause\ntail(.(X52, X53), X53).\nand substitutionT26 -> T36,\nX52 -> T36,\nT27 -> T37,\nX53 -> T37,\nX32 -> T37", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 166 [arrowhead = none ];
166 -> 19;

167 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
19 -> 167 [arrowhead = none ];
167 -> 20;

168 [label="EVAL with clause\nrev([], X60, X61) :- ','(!_6, eq(X60, X61)).\nand substitutionT37 -> [],\nT36 -> T44,\nX60 -> .(T44, []),\nT20 -> T46,\nX61 -> T46,\nT45 -> T46", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 168 [arrowhead = none ];
168 -> 21;

169 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
20 -> 169 [arrowhead = none ];
169 -> 22;

170 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
21 -> 170 [arrowhead = none ];
170 -> 23;

171 [label="ONLY EVAL with clause\nrev(X76, X77, X78) :- ','(head(X76, X79), ','(tail(X76, X80), rev(X80, .(X79, X77), X78))).\nand substitutionT37 -> T59,\nX76 -> T59,\nT36 -> T60,\nX77 -> .(T60, []),\nT20 -> T62,\nX78 -> T62,\nT61 -> T62", fontsize=14, style = filled, fillcolor = lightblue];
22 -> 171 [arrowhead = none ];
171 -> 28;

172 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
23 -> 172 [arrowhead = none ];
172 -> 24;

173 [label="EVAL with clause\neq(X64, X64).\nand substitutionT44 -> T49,\nX64 -> .(T49, []),\nT46 -> .(T49, [])", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 173 [arrowhead = none ];
173 -> 25;

174 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
24 -> 174 [arrowhead = none ];
174 -> 26;

175 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 175 [arrowhead = none ];
175 -> 27;

176 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
28 -> 176 [arrowhead = none ];
176 -> 29;

177 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (rev(T59, .(T60, []), T20), rev([], X60, X61))", fontsize=14, style = filled, fillcolor = lightgreen];
29 -> 177 [arrowhead = none ];
177 -> 30;

178 [label="EVAL with clause\nhead(.(X90, X91), X90).\nand substitutionX90 -> T69,\nX91 -> T70,\nT59 -> .(T69, T70),\nX79 -> T69", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 178 [arrowhead = none ];
178 -> 31;

179 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
30 -> 179 [arrowhead = none ];
179 -> 32;

180 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
31 -> 180 [arrowhead = none ];
180 -> 33;

181 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
33 -> 181 [arrowhead = none ];
181 -> 34;

182 [label="ONLY EVAL with clause\ntail(.(X100, X101), X101).\nand substitutionT69 -> T81,\nX100 -> T81,\nT70 -> T82,\nX101 -> T82,\nX80 -> T82", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 182 [arrowhead = none ];
182 -> 35;

183 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
35 -> 183 [arrowhead = none ];
183 -> 36;

184 [label="EVAL with clause\nrev([], X108, X109) :- ','(!_10, eq(X108, X109)).\nand substitutionT82 -> [],\nT81 -> T92,\nT60 -> T93,\nX108 -> .(T92, .(T93, [])),\nT62 -> T95,\nX109 -> T95,\nT94 -> T95", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 184 [arrowhead = none ];
184 -> 37;

185 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 185 [arrowhead = none ];
185 -> 38;

186 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
37 -> 186 [arrowhead = none ];
186 -> 39;

187 [label="ONLY EVAL with clause\nrev(X124, X125, X126) :- ','(head(X124, X127), ','(tail(X124, X128), rev(X128, .(X127, X125), X126))).\nand substitutionT82 -> T114,\nX124 -> T114,\nT81 -> T115,\nT60 -> T116,\nX125 -> .(T115, .(T116, [])),\nT62 -> T118,\nX126 -> T118,\nT117 -> T118", fontsize=14, style = filled, fillcolor = lightblue];
38 -> 187 [arrowhead = none ];
187 -> 44;

188 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
39 -> 188 [arrowhead = none ];
188 -> 40;

189 [label="EVAL with clause\neq(X112, X112).\nand substitutionT92 -> T100,\nT93 -> T101,\nX112 -> .(T100, .(T101, [])),\nT95 -> .(T100, .(T101, []))", fontsize=14, style = filled, fillcolor = lightblue];
40 -> 189 [arrowhead = none ];
189 -> 41;

190 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
40 -> 190 [arrowhead = none ];
190 -> 42;

191 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
41 -> 191 [arrowhead = none ];
191 -> 43;

192 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
44 -> 192 [arrowhead = none ];
192 -> 45;

193 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (rev(T114, .(T115, .(T116, [])), T62), rev([], X108, X109))", fontsize=14, style = filled, fillcolor = lightgreen];
45 -> 193 [arrowhead = none ];
193 -> 46;

194 [label="EVAL with clause\nhead(.(X138, X139), X138).\nand substitutionX138 -> T126,\nX139 -> T127,\nT114 -> .(T126, T127),\nX127 -> T126", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 194 [arrowhead = none ];
194 -> 47;

195 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
46 -> 195 [arrowhead = none ];
195 -> 48;

196 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
47 -> 196 [arrowhead = none ];
196 -> 49;

197 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
49 -> 197 [arrowhead = none ];
197 -> 50;

198 [label="ONLY EVAL with clause\ntail(.(X148, X149), X149).\nand substitutionT126 -> T140,\nX148 -> T140,\nT127 -> T141,\nX149 -> T141,\nX128 -> T141", fontsize=14, style = filled, fillcolor = lightblue];
50 -> 198 [arrowhead = none ];
198 -> 51;

199 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
51 -> 199 [arrowhead = none ];
199 -> 52;

200 [label="EVAL with clause\nrev([], X156, X157) :- ','(!_14, eq(X156, X157)).\nand substitutionT141 -> [],\nT140 -> T154,\nT115 -> T155,\nT116 -> T156,\nX156 -> .(T154, .(T155, .(T156, []))),\nT118 -> T158,\nX157 -> T158,\nT157 -> T158", fontsize=14, style = filled, fillcolor = lightblue];
52 -> 200 [arrowhead = none ];
200 -> 53;

201 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
52 -> 201 [arrowhead = none ];
201 -> 54;

202 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
53 -> 202 [arrowhead = none ];
202 -> 55;

203 [label="ONLY EVAL with clause\nrev(X172, X173, X174) :- ','(head(X172, X175), ','(tail(X172, X176), rev(X176, .(X175, X173), X174))).\nand substitutionT141 -> T183,\nX172 -> T183,\nT140 -> T184,\nT115 -> T185,\nT116 -> T186,\nX173 -> .(T184, .(T185, .(T186, []))),\nT118 -> T188,\nX174 -> T188,\nT187 -> T188", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 203 [arrowhead = none ];
203 -> 60;

204 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
55 -> 204 [arrowhead = none ];
204 -> 56;

205 [label="EVAL with clause\neq(X160, X160).\nand substitutionT154 -> T165,\nT155 -> T166,\nT156 -> T167,\nX160 -> .(T165, .(T166, .(T167, []))),\nT158 -> .(T165, .(T166, .(T167, [])))", fontsize=14, style = filled, fillcolor = lightblue];
56 -> 205 [arrowhead = none ];
205 -> 57;

206 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
56 -> 206 [arrowhead = none ];
206 -> 58;

207 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
57 -> 207 [arrowhead = none ];
207 -> 59;

208 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
60 -> 208 [arrowhead = none ];
208 -> 61;

209 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (rev(T183, .(T184, .(T185, .(T186, []))), T118), rev([], X156, X157))", fontsize=14, style = filled, fillcolor = lightgreen];
61 -> 209 [arrowhead = none ];
209 -> 62;

210 [label="EVAL with clause\nhead(.(X186, X187), X186).\nand substitutionX186 -> T197,\nX187 -> T198,\nT183 -> .(T197, T198),\nX175 -> T197", fontsize=14, style = filled, fillcolor = lightblue];
62 -> 210 [arrowhead = none ];
210 -> 63;

211 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
62 -> 211 [arrowhead = none ];
211 -> 64;

212 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
63 -> 212 [arrowhead = none ];
212 -> 65;

213 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
65 -> 213 [arrowhead = none ];
213 -> 66;

214 [label="ONLY EVAL with clause\ntail(.(X196, X197), X197).\nand substitutionT197 -> T213,\nX196 -> T213,\nT198 -> T214,\nX197 -> T214,\nX176 -> T214", fontsize=14, style = filled, fillcolor = lightblue];
66 -> 214 [arrowhead = none ];
214 -> 67;

215 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
67 -> 215 [arrowhead = none ];
215 -> 68;

216 [label="EVAL with clause\nrev([], X204, X205) :- ','(!_18, eq(X204, X205)).\nand substitutionT214 -> [],\nT213 -> T230,\nT184 -> T231,\nT185 -> T232,\nT186 -> T233,\nX204 -> .(T230, .(T231, .(T232, .(T233, [])))),\nT188 -> T235,\nX205 -> T235,\nT234 -> T235", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 216 [arrowhead = none ];
216 -> 69;

217 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
68 -> 217 [arrowhead = none ];
217 -> 70;

218 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
69 -> 218 [arrowhead = none ];
218 -> 71;

219 [label="ONLY EVAL with clause\nrev(X220, X221, X222) :- ','(head(X220, X223), ','(tail(X220, X224), rev(X224, .(X223, X221), X222))).\nand substitutionT214 -> T266,\nX220 -> T266,\nT213 -> T267,\nT184 -> T268,\nT185 -> T269,\nT186 -> T270,\nX221 -> .(T267, .(T268, .(T269, .(T270, [])))),\nT188 -> T272,\nX222 -> T272,\nT271 -> T272", fontsize=14, style = filled, fillcolor = lightblue];
70 -> 219 [arrowhead = none ];
219 -> 76;

220 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
71 -> 220 [arrowhead = none ];
220 -> 72;

221 [label="EVAL with clause\neq(X208, X208).\nand substitutionT230 -> T244,\nT231 -> T245,\nT232 -> T246,\nT233 -> T247,\nX208 -> .(T244, .(T245, .(T246, .(T247, [])))),\nT235 -> .(T244, .(T245, .(T246, .(T247, []))))", fontsize=14, style = filled, fillcolor = lightblue];
72 -> 221 [arrowhead = none ];
221 -> 73;

222 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
72 -> 222 [arrowhead = none ];
222 -> 74;

223 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
73 -> 223 [arrowhead = none ];
223 -> 75;

224 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
76 -> 224 [arrowhead = none ];
224 -> 77;

225 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (rev(T266, .(T267, .(T268, .(T269, .(T270, [])))), T188), rev([], X204, X205))", fontsize=14, style = filled, fillcolor = lightgreen];
77 -> 225 [arrowhead = none ];
225 -> 78;

226 [label="EVAL with clause\nhead(.(X234, X235), X234).\nand substitutionX234 -> T282,\nX235 -> T283,\nT266 -> .(T282, T283),\nX223 -> T282", fontsize=14, style = filled, fillcolor = lightblue];
78 -> 226 [arrowhead = none ];
226 -> 79;

227 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
78 -> 227 [arrowhead = none ];
227 -> 80;

228 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
79 -> 228 [arrowhead = none ];
228 -> 81;

229 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
81 -> 229 [arrowhead = none ];
229 -> 82;

230 [label="ONLY EVAL with clause\ntail(.(X244, X245), X245).\nand substitutionT282 -> T300,\nX244 -> T300,\nT283 -> T301,\nX245 -> T301,\nX224 -> T301", fontsize=14, style = filled, fillcolor = lightblue];
82 -> 230 [arrowhead = none ];
230 -> 83;

231 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
83 -> 231 [arrowhead = none ];
231 -> 84;

232 [label="EVAL with clause\nrev([], X252, X253) :- ','(!_22, eq(X252, X253)).\nand substitutionT301 -> [],\nT300 -> T320,\nT267 -> T321,\nT268 -> T322,\nT269 -> T323,\nT270 -> T324,\nX252 -> .(T320, .(T321, .(T322, .(T323, .(T324, []))))),\nT272 -> T326,\nX253 -> T326,\nT325 -> T326", fontsize=14, style = filled, fillcolor = lightblue];
84 -> 232 [arrowhead = none ];
232 -> 85;

233 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
84 -> 233 [arrowhead = none ];
233 -> 86;

234 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
85 -> 234 [arrowhead = none ];
234 -> 87;

235 [label="ONLY EVAL with clause\nrev(X268, X269, X270) :- ','(head(X268, X271), ','(tail(X268, X272), rev(X272, .(X271, X269), X270))).\nand substitutionT301 -> T363,\nX268 -> T363,\nT300 -> T364,\nT267 -> T365,\nT268 -> T366,\nT269 -> T367,\nT270 -> T368,\nX269 -> .(T364, .(T365, .(T366, .(T367, .(T368, []))))),\nT272 -> T370,\nX270 -> T370,\nT369 -> T370", fontsize=14, style = filled, fillcolor = lightblue];
86 -> 235 [arrowhead = none ];
235 -> 92;

236 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
87 -> 236 [arrowhead = none ];
236 -> 88;

237 [label="EVAL with clause\neq(X256, X256).\nand substitutionT320 -> T337,\nT321 -> T338,\nT322 -> T339,\nT323 -> T340,\nT324 -> T341,\nX256 -> .(T337, .(T338, .(T339, .(T340, .(T341, []))))),\nT326 -> .(T337, .(T338, .(T339, .(T340, .(T341, [])))))", fontsize=14, style = filled, fillcolor = lightblue];
88 -> 237 [arrowhead = none ];
237 -> 89;

238 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
88 -> 238 [arrowhead = none ];
238 -> 90;

239 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
89 -> 239 [arrowhead = none ];
239 -> 91;

240 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
92 -> 240 [arrowhead = none ];
240 -> 93;

241 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (rev(T363, .(T364, .(T365, .(T366, .(T367, .(T368, []))))), T272), rev([], X252, X253))", fontsize=14, style = filled, fillcolor = lightgreen];
93 -> 241 [arrowhead = none ];
241 -> 94;

242 [label="EVAL with clause\nhead(.(X282, X283), X282).\nand substitutionX282 -> T381,\nX283 -> T382,\nT363 -> .(T381, T382),\nX271 -> T381", fontsize=14, style = filled, fillcolor = lightblue];
94 -> 242 [arrowhead = none ];
242 -> 95;

243 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
94 -> 243 [arrowhead = none ];
243 -> 96;

244 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
95 -> 244 [arrowhead = none ];
244 -> 97;

245 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
97 -> 245 [arrowhead = none ];
245 -> 98;

246 [label="ONLY EVAL with clause\ntail(.(X292, X293), X293).\nand substitutionT381 -> T401,\nX292 -> T401,\nT382 -> T402,\nX293 -> T402,\nX272 -> T402", fontsize=14, style = filled, fillcolor = lightblue];
98 -> 246 [arrowhead = none ];
246 -> 99;

247 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
99 -> 247 [arrowhead = none ];
247 -> 100;

248 [label="EVAL with clause\nrev([], X300, X301) :- ','(!_26, eq(X300, X301)).\nand substitutionT402 -> [],\nT401 -> T424,\nT364 -> T425,\nT365 -> T426,\nT366 -> T427,\nT367 -> T428,\nT368 -> T429,\nX300 -> .(T424, .(T425, .(T426, .(T427, .(T428, .(T429, [])))))),\nT370 -> T431,\nX301 -> T431,\nT430 -> T431", fontsize=14, style = filled, fillcolor = lightblue];
100 -> 248 [arrowhead = none ];
248 -> 101;

249 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
100 -> 249 [arrowhead = none ];
249 -> 102;

250 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
101 -> 250 [arrowhead = none ];
250 -> 103;

251 [label="ONLY EVAL with clause\nrev(X316, X317, X318) :- ','(head(X316, X319), ','(tail(X316, X320), rev(X320, .(X319, X317), X318))).\nand substitutionT402 -> T474,\nX316 -> T474,\nT401 -> T475,\nT364 -> T476,\nT365 -> T477,\nT366 -> T478,\nT367 -> T479,\nT368 -> T480,\nX317 -> .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, [])))))),\nT370 -> T482,\nX318 -> T482,\nT481 -> T482", fontsize=14, style = filled, fillcolor = lightblue];
102 -> 251 [arrowhead = none ];
251 -> 108;

252 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
103 -> 252 [arrowhead = none ];
252 -> 104;

253 [label="EVAL with clause\neq(X304, X304).\nand substitutionT424 -> T444,\nT425 -> T445,\nT426 -> T446,\nT427 -> T447,\nT428 -> T448,\nT429 -> T449,\nX304 -> .(T444, .(T445, .(T446, .(T447, .(T448, .(T449, [])))))),\nT431 -> .(T444, .(T445, .(T446, .(T447, .(T448, .(T449, []))))))", fontsize=14, style = filled, fillcolor = lightblue];
104 -> 253 [arrowhead = none ];
253 -> 105;

254 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
104 -> 254 [arrowhead = none ];
254 -> 106;

255 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
105 -> 255 [arrowhead = none ];
255 -> 107;

256 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
108 -> 256 [arrowhead = none ];
256 -> 109;

257 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (rev(T474, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, [])))))), T370), rev([], X300, X301))", fontsize=14, style = filled, fillcolor = lightgreen];
109 -> 257 [arrowhead = none ];
257 -> 110;

258 [label="EVAL with clause\nhead(.(X330, X331), X330).\nand substitutionX330 -> T494,\nX331 -> T495,\nT474 -> .(T494, T495),\nX319 -> T494", fontsize=14, style = filled, fillcolor = lightblue];
110 -> 258 [arrowhead = none ];
258 -> 111;

259 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
110 -> 259 [arrowhead = none ];
259 -> 112;

260 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
111 -> 260 [arrowhead = none ];
260 -> 113;

261 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
113 -> 261 [arrowhead = none ];
261 -> 114;

262 [label="ONLY EVAL with clause\ntail(.(X340, X341), X341).\nand substitutionT494 -> T516,\nX340 -> T516,\nT495 -> T517,\nX341 -> T517,\nX320 -> T517", fontsize=14, style = filled, fillcolor = lightblue];
114 -> 262 [arrowhead = none ];
262 -> 115;

263 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
115 -> 263 [arrowhead = none ];
263 -> 116;

264 [label="EVAL with clause\nrev([], X348, X349) :- ','(!_30, eq(X348, X349)).\nand substitutionT517 -> [],\nT516 -> T542,\nT475 -> T543,\nT476 -> T544,\nT477 -> T545,\nT478 -> T546,\nT479 -> T547,\nT480 -> T548,\nX348 -> .(T542, .(T543, .(T544, .(T545, .(T546, .(T547, .(T548, []))))))),\nT482 -> T550,\nX349 -> T550,\nT549 -> T550", fontsize=14, style = filled, fillcolor = lightblue];
116 -> 264 [arrowhead = none ];
264 -> 117;

265 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
116 -> 265 [arrowhead = none ];
265 -> 118;

266 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
117 -> 266 [arrowhead = none ];
266 -> 119;

267 [label="ONLY EVAL with clause\nrev(X364, X365, X366) :- ','(head(X364, X367), ','(tail(X364, X368), rev(X368, .(X367, X365), X366))).\nand substitutionT517 -> T599,\nX364 -> T599,\nT516 -> T600,\nT475 -> T601,\nT476 -> T602,\nT477 -> T603,\nT478 -> T604,\nT479 -> T605,\nT480 -> T606,\nX365 -> .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, []))))))),\nT482 -> T608,\nX366 -> T608,\nT607 -> T608", fontsize=14, style = filled, fillcolor = lightblue];
118 -> 267 [arrowhead = none ];
267 -> 124;

268 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
119 -> 268 [arrowhead = none ];
268 -> 120;

269 [label="EVAL with clause\neq(X352, X352).\nand substitutionT542 -> T565,\nT543 -> T566,\nT544 -> T567,\nT545 -> T568,\nT546 -> T569,\nT547 -> T570,\nT548 -> T571,\nX352 -> .(T565, .(T566, .(T567, .(T568, .(T569, .(T570, .(T571, []))))))),\nT550 -> .(T565, .(T566, .(T567, .(T568, .(T569, .(T570, .(T571, [])))))))", fontsize=14, style = filled, fillcolor = lightblue];
120 -> 269 [arrowhead = none ];
269 -> 121;

270 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
120 -> 270 [arrowhead = none ];
270 -> 122;

271 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
121 -> 271 [arrowhead = none ];
271 -> 123;

272 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
124 -> 272 [arrowhead = none ];
272 -> 125;

273 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (rev(T599, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, []))))))), T482), rev([], X348, X349))", fontsize=14, style = filled, fillcolor = lightgreen];
125 -> 273 [arrowhead = none ];
273 -> 126;

274 [label="EVAL with clause\nhead(.(X378, X379), X378).\nand substitutionX378 -> T621,\nX379 -> T622,\nT599 -> .(T621, T622),\nX367 -> T621", fontsize=14, style = filled, fillcolor = lightblue];
126 -> 274 [arrowhead = none ];
274 -> 127;

275 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
126 -> 275 [arrowhead = none ];
275 -> 128;

276 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
127 -> 276 [arrowhead = none ];
276 -> 129;

277 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
129 -> 277 [arrowhead = none ];
277 -> 130;

278 [label="ONLY EVAL with clause\ntail(.(X388, X389), X389).\nand substitutionT621 -> T645,\nX388 -> T645,\nT622 -> T646,\nX389 -> T646,\nX368 -> T646", fontsize=14, style = filled, fillcolor = lightblue];
130 -> 278 [arrowhead = none ];
278 -> 131;

279 [label="GENERALIZATION\nT656 <-- .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, [])))))))\n\nNew Knowledge:\nT656 is ground", fontsize=14, style = filled, fillcolor = violet];
131 -> 279 [arrowhead = none ];
279 -> 132;

280 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
132 -> 280 [arrowhead = none ];
280 -> 133;

281 [label="EVAL with clause\nrev([], X398, X399) :- ','(!_34, eq(X398, X399)).\nand substitutionT646 -> [],\nT645 -> T666,\nT656 -> T667,\nX398 -> .(T666, T667),\nT608 -> T669,\nX399 -> T669,\nT668 -> T669", fontsize=14, style = filled, fillcolor = lightblue];
133 -> 281 [arrowhead = none ];
281 -> 134;

282 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
133 -> 282 [arrowhead = none ];
282 -> 135;

283 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
134 -> 283 [arrowhead = none ];
283 -> 136;

284 [label="ONLY EVAL with clause\nrev(X414, X415, X416) :- ','(head(X414, X417), ','(tail(X414, X418), rev(X418, .(X417, X415), X416))).\nand substitutionT646 -> T688,\nX414 -> T688,\nT645 -> T689,\nT656 -> T690,\nX415 -> .(T689, T690),\nT608 -> T692,\nX416 -> T692,\nT691 -> T692", fontsize=14, style = filled, fillcolor = lightblue];
135 -> 284 [arrowhead = none ];
284 -> 141;

285 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
136 -> 285 [arrowhead = none ];
285 -> 137;

286 [label="EVAL with clause\neq(X402, X402).\nand substitutionT666 -> T674,\nT667 -> T675,\nX402 -> .(T674, T675),\nT669 -> .(T674, T675)", fontsize=14, style = filled, fillcolor = lightblue];
137 -> 286 [arrowhead = none ];
286 -> 138;

287 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
137 -> 287 [arrowhead = none ];
287 -> 139;

288 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
138 -> 288 [arrowhead = none ];
288 -> 140;

289 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
141 -> 289 [arrowhead = none ];
289 -> 142;

290 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (rev(T688, .(T689, T690), T608), rev([], X398, X399))", fontsize=14, style = filled, fillcolor = lightgreen];
142 -> 290 [arrowhead = none ];
290 -> 143;

291 [label="EVAL with clause\nhead(.(X428, X429), X428).\nand substitutionX428 -> T700,\nX429 -> T701,\nT688 -> .(T700, T701),\nX417 -> T700", fontsize=14, style = filled, fillcolor = lightblue];
143 -> 291 [arrowhead = none ];
291 -> 144;

292 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
143 -> 292 [arrowhead = none ];
292 -> 145;

293 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
144 -> 293 [arrowhead = none ];
293 -> 146;

294 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
146 -> 294 [arrowhead = none ];
294 -> 147;

295 [label="ONLY EVAL with clause\ntail(.(X438, X439), X439).\nand substitutionT700 -> T714,\nX438 -> T714,\nT701 -> T715,\nX439 -> T715,\nX418 -> T715", fontsize=14, style = filled, fillcolor = lightblue];
147 -> 295 [arrowhead = none ];
295 -> 148;

296 [label="INSTANCE with matching:\nT646 -> T715\nT645 -> T714\nT656 -> .(T689, T690)\nT608 -> T692", fontsize=14, style = filled, fillcolor = lightgrey];
148 -> 296 [arrowhead = none , style=dashed];
296 -> 132[style=dashed];

}

(2) Obligation:

Clauses:

revA([], T674, T675, .(T674, T675)).
revA(.(T714, T715), T689, T690, T692) :- revA(T715, T714, .(T689, T690), T692).
revB([], []).
revB(.(T49, []), .(T49, [])).
revB(.(T101, .(T100, [])), .(T100, .(T101, []))).
revB(.(T167, .(T166, .(T165, []))), .(T165, .(T166, .(T167, [])))).
revB(.(T247, .(T246, .(T245, .(T244, [])))), .(T244, .(T245, .(T246, .(T247, []))))).
revB(.(T341, .(T340, .(T339, .(T338, .(T337, []))))), .(T337, .(T338, .(T339, .(T340, .(T341, [])))))).
revB(.(T449, .(T448, .(T447, .(T446, .(T445, .(T444, [])))))), .(T444, .(T445, .(T446, .(T447, .(T448, .(T449, []))))))).
revB(.(T571, .(T570, .(T569, .(T568, .(T567, .(T566, .(T565, []))))))), .(T565, .(T566, .(T567, .(T568, .(T569, .(T570, .(T571, [])))))))).
revB(.(T606, .(T605, .(T604, .(T603, .(T602, .(T601, .(T600, .(T645, T646)))))))), T608) :- revA(T646, T645, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, []))))))), T608).

Query: revB(g,a)

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
revB_in: (b,f)
revA_in: (b,b,b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

revB_in_ga([], []) → revB_out_ga([], [])
revB_in_ga(.(T49, []), .(T49, [])) → revB_out_ga(.(T49, []), .(T49, []))
revB_in_ga(.(T101, .(T100, [])), .(T100, .(T101, []))) → revB_out_ga(.(T101, .(T100, [])), .(T100, .(T101, [])))
revB_in_ga(.(T167, .(T166, .(T165, []))), .(T165, .(T166, .(T167, [])))) → revB_out_ga(.(T167, .(T166, .(T165, []))), .(T165, .(T166, .(T167, []))))
revB_in_ga(.(T247, .(T246, .(T245, .(T244, [])))), .(T244, .(T245, .(T246, .(T247, []))))) → revB_out_ga(.(T247, .(T246, .(T245, .(T244, [])))), .(T244, .(T245, .(T246, .(T247, [])))))
revB_in_ga(.(T341, .(T340, .(T339, .(T338, .(T337, []))))), .(T337, .(T338, .(T339, .(T340, .(T341, [])))))) → revB_out_ga(.(T341, .(T340, .(T339, .(T338, .(T337, []))))), .(T337, .(T338, .(T339, .(T340, .(T341, []))))))
revB_in_ga(.(T449, .(T448, .(T447, .(T446, .(T445, .(T444, [])))))), .(T444, .(T445, .(T446, .(T447, .(T448, .(T449, []))))))) → revB_out_ga(.(T449, .(T448, .(T447, .(T446, .(T445, .(T444, [])))))), .(T444, .(T445, .(T446, .(T447, .(T448, .(T449, [])))))))
revB_in_ga(.(T571, .(T570, .(T569, .(T568, .(T567, .(T566, .(T565, []))))))), .(T565, .(T566, .(T567, .(T568, .(T569, .(T570, .(T571, [])))))))) → revB_out_ga(.(T571, .(T570, .(T569, .(T568, .(T567, .(T566, .(T565, []))))))), .(T565, .(T566, .(T567, .(T568, .(T569, .(T570, .(T571, []))))))))
revB_in_ga(.(T606, .(T605, .(T604, .(T603, .(T602, .(T601, .(T600, .(T645, T646)))))))), T608) → U2_ga(T606, T605, T604, T603, T602, T601, T600, T645, T646, T608, revA_in_ggga(T646, T645, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, []))))))), T608))
revA_in_ggga([], T674, T675, .(T674, T675)) → revA_out_ggga([], T674, T675, .(T674, T675))
revA_in_ggga(.(T714, T715), T689, T690, T692) → U1_ggga(T714, T715, T689, T690, T692, revA_in_ggga(T715, T714, .(T689, T690), T692))
U1_ggga(T714, T715, T689, T690, T692, revA_out_ggga(T715, T714, .(T689, T690), T692)) → revA_out_ggga(.(T714, T715), T689, T690, T692)
U2_ga(T606, T605, T604, T603, T602, T601, T600, T645, T646, T608, revA_out_ggga(T646, T645, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, []))))))), T608)) → revB_out_ga(.(T606, .(T605, .(T604, .(T603, .(T602, .(T601, .(T600, .(T645, T646)))))))), T608)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

revB_in_ga([], []) → revB_out_ga([], [])
revB_in_ga(.(T49, []), .(T49, [])) → revB_out_ga(.(T49, []), .(T49, []))
revB_in_ga(.(T101, .(T100, [])), .(T100, .(T101, []))) → revB_out_ga(.(T101, .(T100, [])), .(T100, .(T101, [])))
revB_in_ga(.(T167, .(T166, .(T165, []))), .(T165, .(T166, .(T167, [])))) → revB_out_ga(.(T167, .(T166, .(T165, []))), .(T165, .(T166, .(T167, []))))
revB_in_ga(.(T247, .(T246, .(T245, .(T244, [])))), .(T244, .(T245, .(T246, .(T247, []))))) → revB_out_ga(.(T247, .(T246, .(T245, .(T244, [])))), .(T244, .(T245, .(T246, .(T247, [])))))
revB_in_ga(.(T341, .(T340, .(T339, .(T338, .(T337, []))))), .(T337, .(T338, .(T339, .(T340, .(T341, [])))))) → revB_out_ga(.(T341, .(T340, .(T339, .(T338, .(T337, []))))), .(T337, .(T338, .(T339, .(T340, .(T341, []))))))
revB_in_ga(.(T449, .(T448, .(T447, .(T446, .(T445, .(T444, [])))))), .(T444, .(T445, .(T446, .(T447, .(T448, .(T449, []))))))) → revB_out_ga(.(T449, .(T448, .(T447, .(T446, .(T445, .(T444, [])))))), .(T444, .(T445, .(T446, .(T447, .(T448, .(T449, [])))))))
revB_in_ga(.(T571, .(T570, .(T569, .(T568, .(T567, .(T566, .(T565, []))))))), .(T565, .(T566, .(T567, .(T568, .(T569, .(T570, .(T571, [])))))))) → revB_out_ga(.(T571, .(T570, .(T569, .(T568, .(T567, .(T566, .(T565, []))))))), .(T565, .(T566, .(T567, .(T568, .(T569, .(T570, .(T571, []))))))))
revB_in_ga(.(T606, .(T605, .(T604, .(T603, .(T602, .(T601, .(T600, .(T645, T646)))))))), T608) → U2_ga(T606, T605, T604, T603, T602, T601, T600, T645, T646, T608, revA_in_ggga(T646, T645, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, []))))))), T608))
revA_in_ggga([], T674, T675, .(T674, T675)) → revA_out_ggga([], T674, T675, .(T674, T675))
revA_in_ggga(.(T714, T715), T689, T690, T692) → U1_ggga(T714, T715, T689, T690, T692, revA_in_ggga(T715, T714, .(T689, T690), T692))
U1_ggga(T714, T715, T689, T690, T692, revA_out_ggga(T715, T714, .(T689, T690), T692)) → revA_out_ggga(.(T714, T715), T689, T690, T692)
U2_ga(T606, T605, T604, T603, T602, T601, T600, T645, T646, T608, revA_out_ggga(T646, T645, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, []))))))), T608)) → revB_out_ga(.(T606, .(T605, .(T604, .(T603, .(T602, .(T601, .(T600, .(T645, T646)))))))), T608)

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

REVB_IN_GA(.(T606, .(T605, .(T604, .(T603, .(T602, .(T601, .(T600, .(T645, T646)))))))), T608) → U2_GA(T606, T605, T604, T603, T602, T601, T600, T645, T646, T608, revA_in_ggga(T646, T645, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, []))))))), T608))
REVB_IN_GA(.(T606, .(T605, .(T604, .(T603, .(T602, .(T601, .(T600, .(T645, T646)))))))), T608) → REVA_IN_GGGA(T646, T645, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, []))))))), T608)
REVA_IN_GGGA(.(T714, T715), T689, T690, T692) → U1_GGGA(T714, T715, T689, T690, T692, revA_in_ggga(T715, T714, .(T689, T690), T692))
REVA_IN_GGGA(.(T714, T715), T689, T690, T692) → REVA_IN_GGGA(T715, T714, .(T689, T690), T692)

The TRS R consists of the following rules:

revB_in_ga([], []) → revB_out_ga([], [])
revB_in_ga(.(T49, []), .(T49, [])) → revB_out_ga(.(T49, []), .(T49, []))
revB_in_ga(.(T101, .(T100, [])), .(T100, .(T101, []))) → revB_out_ga(.(T101, .(T100, [])), .(T100, .(T101, [])))
revB_in_ga(.(T167, .(T166, .(T165, []))), .(T165, .(T166, .(T167, [])))) → revB_out_ga(.(T167, .(T166, .(T165, []))), .(T165, .(T166, .(T167, []))))
revB_in_ga(.(T247, .(T246, .(T245, .(T244, [])))), .(T244, .(T245, .(T246, .(T247, []))))) → revB_out_ga(.(T247, .(T246, .(T245, .(T244, [])))), .(T244, .(T245, .(T246, .(T247, [])))))
revB_in_ga(.(T341, .(T340, .(T339, .(T338, .(T337, []))))), .(T337, .(T338, .(T339, .(T340, .(T341, [])))))) → revB_out_ga(.(T341, .(T340, .(T339, .(T338, .(T337, []))))), .(T337, .(T338, .(T339, .(T340, .(T341, []))))))
revB_in_ga(.(T449, .(T448, .(T447, .(T446, .(T445, .(T444, [])))))), .(T444, .(T445, .(T446, .(T447, .(T448, .(T449, []))))))) → revB_out_ga(.(T449, .(T448, .(T447, .(T446, .(T445, .(T444, [])))))), .(T444, .(T445, .(T446, .(T447, .(T448, .(T449, [])))))))
revB_in_ga(.(T571, .(T570, .(T569, .(T568, .(T567, .(T566, .(T565, []))))))), .(T565, .(T566, .(T567, .(T568, .(T569, .(T570, .(T571, [])))))))) → revB_out_ga(.(T571, .(T570, .(T569, .(T568, .(T567, .(T566, .(T565, []))))))), .(T565, .(T566, .(T567, .(T568, .(T569, .(T570, .(T571, []))))))))
revB_in_ga(.(T606, .(T605, .(T604, .(T603, .(T602, .(T601, .(T600, .(T645, T646)))))))), T608) → U2_ga(T606, T605, T604, T603, T602, T601, T600, T645, T646, T608, revA_in_ggga(T646, T645, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, []))))))), T608))
revA_in_ggga([], T674, T675, .(T674, T675)) → revA_out_ggga([], T674, T675, .(T674, T675))
revA_in_ggga(.(T714, T715), T689, T690, T692) → U1_ggga(T714, T715, T689, T690, T692, revA_in_ggga(T715, T714, .(T689, T690), T692))
U1_ggga(T714, T715, T689, T690, T692, revA_out_ggga(T715, T714, .(T689, T690), T692)) → revA_out_ggga(.(T714, T715), T689, T690, T692)
U2_ga(T606, T605, T604, T603, T602, T601, T600, T645, T646, T608, revA_out_ggga(T646, T645, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, []))))))), T608)) → revB_out_ga(.(T606, .(T605, .(T604, .(T603, .(T602, .(T601, .(T600, .(T645, T646)))))))), T608)

The argument filtering Pi contains the following mapping:
revB_in_ga(x1, x2) = revB_in_ga(x1)
[] = []
revB_out_ga(x1, x2) = revB_out_ga(x2)
.(x1, x2) = .(x1, x2)
U2_ga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = U2_ga(x11)
revA_in_ggga(x1, x2, x3, x4) = revA_in_ggga(x1, x2, x3)
revA_out_ggga(x1, x2, x3, x4) = revA_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5, x6) = U1_ggga(x6)
REVB_IN_GA(x1, x2) = REVB_IN_GA(x1)
U2_GA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = U2_GA(x11)
REVA_IN_GGGA(x1, x2, x3, x4) = REVA_IN_GGGA(x1, x2, x3)
U1_GGGA(x1, x2, x3, x4, x5, x6) = U1_GGGA(x6)

We have to consider all (P,R,Pi)-chains

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

REVB_IN_GA(.(T606, .(T605, .(T604, .(T603, .(T602, .(T601, .(T600, .(T645, T646)))))))), T608) → U2_GA(T606, T605, T604, T603, T602, T601, T600, T645, T646, T608, revA_in_ggga(T646, T645, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, []))))))), T608))
REVB_IN_GA(.(T606, .(T605, .(T604, .(T603, .(T602, .(T601, .(T600, .(T645, T646)))))))), T608) → REVA_IN_GGGA(T646, T645, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, []))))))), T608)
REVA_IN_GGGA(.(T714, T715), T689, T690, T692) → U1_GGGA(T714, T715, T689, T690, T692, revA_in_ggga(T715, T714, .(T689, T690), T692))
REVA_IN_GGGA(.(T714, T715), T689, T690, T692) → REVA_IN_GGGA(T715, T714, .(T689, T690), T692)

The TRS R consists of the following rules:

revB_in_ga([], []) → revB_out_ga([], [])
revB_in_ga(.(T49, []), .(T49, [])) → revB_out_ga(.(T49, []), .(T49, []))
revB_in_ga(.(T101, .(T100, [])), .(T100, .(T101, []))) → revB_out_ga(.(T101, .(T100, [])), .(T100, .(T101, [])))
revB_in_ga(.(T167, .(T166, .(T165, []))), .(T165, .(T166, .(T167, [])))) → revB_out_ga(.(T167, .(T166, .(T165, []))), .(T165, .(T166, .(T167, []))))
revB_in_ga(.(T247, .(T246, .(T245, .(T244, [])))), .(T244, .(T245, .(T246, .(T247, []))))) → revB_out_ga(.(T247, .(T246, .(T245, .(T244, [])))), .(T244, .(T245, .(T246, .(T247, [])))))
revB_in_ga(.(T341, .(T340, .(T339, .(T338, .(T337, []))))), .(T337, .(T338, .(T339, .(T340, .(T341, [])))))) → revB_out_ga(.(T341, .(T340, .(T339, .(T338, .(T337, []))))), .(T337, .(T338, .(T339, .(T340, .(T341, []))))))
revB_in_ga(.(T449, .(T448, .(T447, .(T446, .(T445, .(T444, [])))))), .(T444, .(T445, .(T446, .(T447, .(T448, .(T449, []))))))) → revB_out_ga(.(T449, .(T448, .(T447, .(T446, .(T445, .(T444, [])))))), .(T444, .(T445, .(T446, .(T447, .(T448, .(T449, [])))))))
revB_in_ga(.(T571, .(T570, .(T569, .(T568, .(T567, .(T566, .(T565, []))))))), .(T565, .(T566, .(T567, .(T568, .(T569, .(T570, .(T571, [])))))))) → revB_out_ga(.(T571, .(T570, .(T569, .(T568, .(T567, .(T566, .(T565, []))))))), .(T565, .(T566, .(T567, .(T568, .(T569, .(T570, .(T571, []))))))))
revB_in_ga(.(T606, .(T605, .(T604, .(T603, .(T602, .(T601, .(T600, .(T645, T646)))))))), T608) → U2_ga(T606, T605, T604, T603, T602, T601, T600, T645, T646, T608, revA_in_ggga(T646, T645, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, []))))))), T608))
revA_in_ggga([], T674, T675, .(T674, T675)) → revA_out_ggga([], T674, T675, .(T674, T675))
revA_in_ggga(.(T714, T715), T689, T690, T692) → U1_ggga(T714, T715, T689, T690, T692, revA_in_ggga(T715, T714, .(T689, T690), T692))
U1_ggga(T714, T715, T689, T690, T692, revA_out_ggga(T715, T714, .(T689, T690), T692)) → revA_out_ggga(.(T714, T715), T689, T690, T692)
U2_ga(T606, T605, T604, T603, T602, T601, T600, T645, T646, T608, revA_out_ggga(T646, T645, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, []))))))), T608)) → revB_out_ga(.(T606, .(T605, .(T604, .(T603, .(T602, .(T601, .(T600, .(T645, T646)))))))), T608)

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 3 less nodes.

(8) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

REVA_IN_GGGA(.(T714, T715), T689, T690, T692) → REVA_IN_GGGA(T715, T714, .(T689, T690), T692)

The TRS R consists of the following rules:

revB_in_ga([], []) → revB_out_ga([], [])
revB_in_ga(.(T49, []), .(T49, [])) → revB_out_ga(.(T49, []), .(T49, []))
revB_in_ga(.(T101, .(T100, [])), .(T100, .(T101, []))) → revB_out_ga(.(T101, .(T100, [])), .(T100, .(T101, [])))
revB_in_ga(.(T167, .(T166, .(T165, []))), .(T165, .(T166, .(T167, [])))) → revB_out_ga(.(T167, .(T166, .(T165, []))), .(T165, .(T166, .(T167, []))))
revB_in_ga(.(T247, .(T246, .(T245, .(T244, [])))), .(T244, .(T245, .(T246, .(T247, []))))) → revB_out_ga(.(T247, .(T246, .(T245, .(T244, [])))), .(T244, .(T245, .(T246, .(T247, [])))))
revB_in_ga(.(T341, .(T340, .(T339, .(T338, .(T337, []))))), .(T337, .(T338, .(T339, .(T340, .(T341, [])))))) → revB_out_ga(.(T341, .(T340, .(T339, .(T338, .(T337, []))))), .(T337, .(T338, .(T339, .(T340, .(T341, []))))))
revB_in_ga(.(T449, .(T448, .(T447, .(T446, .(T445, .(T444, [])))))), .(T444, .(T445, .(T446, .(T447, .(T448, .(T449, []))))))) → revB_out_ga(.(T449, .(T448, .(T447, .(T446, .(T445, .(T444, [])))))), .(T444, .(T445, .(T446, .(T447, .(T448, .(T449, [])))))))
revB_in_ga(.(T571, .(T570, .(T569, .(T568, .(T567, .(T566, .(T565, []))))))), .(T565, .(T566, .(T567, .(T568, .(T569, .(T570, .(T571, [])))))))) → revB_out_ga(.(T571, .(T570, .(T569, .(T568, .(T567, .(T566, .(T565, []))))))), .(T565, .(T566, .(T567, .(T568, .(T569, .(T570, .(T571, []))))))))
revB_in_ga(.(T606, .(T605, .(T604, .(T603, .(T602, .(T601, .(T600, .(T645, T646)))))))), T608) → U2_ga(T606, T605, T604, T603, T602, T601, T600, T645, T646, T608, revA_in_ggga(T646, T645, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, []))))))), T608))
revA_in_ggga([], T674, T675, .(T674, T675)) → revA_out_ggga([], T674, T675, .(T674, T675))
revA_in_ggga(.(T714, T715), T689, T690, T692) → U1_ggga(T714, T715, T689, T690, T692, revA_in_ggga(T715, T714, .(T689, T690), T692))
U1_ggga(T714, T715, T689, T690, T692, revA_out_ggga(T715, T714, .(T689, T690), T692)) → revA_out_ggga(.(T714, T715), T689, T690, T692)
U2_ga(T606, T605, T604, T603, T602, T601, T600, T645, T646, T608, revA_out_ggga(T646, T645, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, []))))))), T608)) → revB_out_ga(.(T606, .(T605, .(T604, .(T603, .(T602, .(T601, .(T600, .(T645, T646)))))))), T608)

The argument filtering Pi contains the following mapping:
revB_in_ga(x1, x2) = revB_in_ga(x1)
[] = []
revB_out_ga(x1, x2) = revB_out_ga(x2)
.(x1, x2) = .(x1, x2)
U2_ga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = U2_ga(x11)
revA_in_ggga(x1, x2, x3, x4) = revA_in_ggga(x1, x2, x3)
revA_out_ggga(x1, x2, x3, x4) = revA_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5, x6) = U1_ggga(x6)
REVA_IN_GGGA(x1, x2, x3, x4) = REVA_IN_GGGA(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(9) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(10) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

REVA_IN_GGGA(.(T714, T715), T689, T690, T692) → REVA_IN_GGGA(T715, T714, .(T689, T690), T692)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
REVA_IN_GGGA(x1, x2, x3, x4) = REVA_IN_GGGA(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(11) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(12) Obligation:

Q DP problem:
The TRS P consists of the following rules:

REVA_IN_GGGA(.(T714, T715), T689, T690) → REVA_IN_GGGA(T715, T714, .(T689, T690))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(13) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

REVA_IN_GGGA(.(T714, T715), T689, T690) → REVA_IN_GGGA(T715, T714, .(T689, T690))
The graph contains the following edges 1 > 1, 1 > 2

(0) Obligation:

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) PrologToPiTRSProof (SOUND transformation)

(4) Obligation:

(5) DependencyPairsProof (EQUIVALENT transformation)

(6) Obligation:

(7) DependencyGraphProof (EQUIVALENT transformation)

(8) Obligation:

(9) UsableRulesProof (EQUIVALENT transformation)

(10) Obligation:

(11) PiDPToQDPProof (SOUND transformation)

(12) Obligation:

(13) QDPSizeChangeProof (EQUIVALENT transformation)

(14) YES